k:Knd, L:IdLnk List. k sends only on links in L  MsgA 

latex

Definitions	Id, t  T, Knd, type List, x.A(x), x. t(x), x:A. B(x), , IdLnk, x : v, x:AB(x), Void, Type, Top, x:AB(x), State(ds), Prop, mk-ma, k sends only on links in L, MsgA
Lemmas	mk-ma wf, ma-state wf, top wf, fpf-single wf, IdLnk wf, fpf-empty wf, Knd wf, Id wf